module TravelDream

sig UString {}
sig posInt  { value: Int} {value > 0}

sig Customer
{
id:one posInt,
username:one UString,
password:one UString,
firstname:one UString,
lastname:one UString,
email:one UString,
phone:lone UString,
PersonalPackages: seq Personal_Package
}
{
username != email
}

sig Employee
{
id:one posInt,
username:one UString,
password:one UString,
firstname:one UString,
lastname:one UString,
email:one UString,
phone:lone UString,
managef: seq Flight,
manageh: seq Hotel,
managee:seq Excursion,
managep: seq Preplanned_Package
}
{
username != email
}


sig Flight
{
id:one posInt,
name: one UString,
arrival_airport:one UString,
departure_airport:one UString,
flight_duration:one UString,
price:one posInt,
details:one UString
}

sig Hotel
{
id:one posInt,
name: one UString,
country:one UString,
city:one UString,
address:one UString,
rate: one Int,
price:one posInt,
details:one UString
}
{
rate > 0
rate <= 5
}
sig Excursion
{
id:one posInt,
title: one UString,
country:one UString,
place:one UString,
address:one UString,
rate: one Int,
price:one posInt,
details:one UString
}
{
rate > 0
rate <= 5
}

sig Preplanned_Package
{
id: one posInt,
p1: one Flight,
p2: one Hotel,
p3: one Excursion,
}

sig Personal_Package
{
id: one posInt,
pppackage: one Preplanned_Package,
departure_date: lone UString,
return_date: lone UString,
hotel_options:lone UString,
status: one UString,
}

//-------------------------------NO DUPLICATE IDS------------------------

fact NoDuplicateId{
no disj e1,e2:Employee|e1.id=e2.id
no disj c1,c2:Customer|c1.id=c2.id
no disj e1,e2:Flight|e1.id=e2.id
no disj e1,e2:Hotel|e1.id=e2.id
no disj e1,e2:Excursion|e1.id=e2.id
no disj e1,e2:Preplanned_Package|e1.id=e2.id
no disj e1,e2:Personal_Package|e1.id=e2.id
}

//---------------------- NO DUPLICATE EMPLOYEE OR CUSTOMER
// but I allow the same person to be have both a customer and an employee account.
fact NoDuplicateEntity {
    no disj e1,e2:Employee | e1.username=e2.username || e1.email=e2.email
    no disj c1, c2:Customer | c1.username=c2.username || c1.email=c2.email
    no disj c1, c2:Flight | c1.name=c2.name
    no disj c1, c2:Excursion| c1.title=c2.title
    no disj c1, c2:Preplanned_Package| c1.p1=c2.p1 && c1.p2=c2.p2 && c1.p3=c2.p3
} 
assert A_NoDuplicateEntity{
    no disj e1,e2:Employee | e1.username=e2.username || e1.email=e2.email
    no disj c1, c2:Customer | c1.username=c2.username || c1.email=c2.email
    no disj c1, c2:Flight | c1.name=c2.name
    no disj c1, c2:Excursion| c1.title=c2.title
    no disj c1, c2:Preplanned_Package| c1.p1=c2.p1 && c1.p2=c2.p2 && c1.p3=c2.p3
}
check A_NoDuplicateEntity for 4

//--------------------Every Personal Package belongs to a customer--------------
fact PPackagebelongcustomer {
    all p:Personal_Package {
			one c:Customer | p in c.PersonalPackages.elems
	   }
} 

assert A_PPackagebelongcustomer{
   all p:Personal_Package {
			one c:Customer | p in c.PersonalPackages.elems
	   }
}
check A_PPackagebelongcustomer for 4

//--------------------Every Employee manages all products and predefined packages-------------
fact EmployeeManageppdp {
    all e:Employee {
			all f:Flight | f in e.managef.elems
			all h:Hotel | h in e.manageh.elems
			all ex:Excursion | ex in e.managee.elems 
			all p:Preplanned_Package | p in e.managep.elems
	   }
} 

assert A_EmployeeManageppdp{
   all e:Employee {
			all f:Flight | f in e.managef.elems
			all h:Hotel | h in e.manageh.elems
			all ex:Excursion | ex in e.managee.elems 
			all p:Preplanned_Package | p in e.managep.elems
	   }
}
check A_EmployeeManageppdp for 4

//---------------------No Duplicates in arrays-------------------
fact NoDuplicatesInArrays{
		all e:Employee | !e.managef.hasDups && !e.manageh.hasDups && !e.managee.hasDups && !e.managep.hasDups
		all c:Customer | !c.PersonalPackages.hasDups
}
assert A_NoDuplicatesInArrays{
    	all e:Employee | !e.managef.hasDups && !e.manageh.hasDups && !e.managee.hasDups && !e.managep.hasDups
		all c:Customer | !c.PersonalPackages.hasDups
}
check A_NoDuplicatesInArrays for 4

pred show()
{
#Personal_Package > 2
#Employee = 2
#Hotel = 1
#Flight > 2
#Customer  > 1
#Customer  <= 5
}
run show for 3

